\begin{tabbing}
$\forall$\=$k$:Knd, $l$:IdLnk, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$a$:Knd fp$\rightarrow$ Type, $f$:(Id$\times$Top) List, $l_{1}$:IdLnk, ${\it tg}$:Id,\+
\\[0ex]$L$:Knd List.
\-\\[0ex]($l$ $=$ $l_{1}$ $\Rightarrow$ (${\it tg}$ $\in$ map($\lambda$$p$.1of($p$);$f$)) $\Rightarrow$ ($k$ $\in$ $L$))
\\[0ex]$\Rightarrow$ (with declarations ds:${\it ds}$da:${\it da}$$k$(v) sends $f$ s v on link $l$ $\Vert\!+$ only $L$ sends on ($l_{1}$ with ${\it tg}$))
\end{tabbing}